“Euclid taught me that without assumptions there is no proof. Therefore, in any argument, examine the assumptions.” - E. T. Bell
If we want to show \[ (P\to Q), (Q\to R), (R\to S), (S\to T), (T\to U) \vDash (P \to U) \] it is tedious to enumerate and check all \(2^6=64\) relevant models.
Even simpler examples can take a lot of work to verify.
Example
Here we confirm that \(R\) follows logically from \(P\), \(P\to Q\), and \(Q\to R\):
| \(P\) | \(Q\) | \(R\) | \(P\) | \(P\to Q\) | \(Q\to R\) | \(R\) |
|---|---|---|---|---|---|---|
| T | T | T | T | T | T | T |
| T | T | F | T | T | F | F |
| T | F | T | T | F | T | T |
| T | F | F | T | F | T | F |
| F | T | T | F | T | T | T |
| F | T | F | F | T | F | F |
| F | F | T | F | T | T | T |
| F | F | F | F | T | T | F |
In all the models (all one of them) where the three assumptions are true, the conclusion is true as well.
Worse, the logic we’ve been considering is a basic logical system that can model only fairly simple arguments. To capture real-world reasoning we will need to move from Propositional Logic to Predicate Logic (also called First-Order Logic), where verifying entailments requires checking infinitely many models!
So while entailment does capture the defining property of correct reasoning (\({\cal B}\) follows logically from \({\cal A}\) iff there’s no situation where \({\cal A}\) is true but \({\cal B}\) is false) entailment is often inconvenient to work with directly.
(At least when we want to show an inference is correct. If we want to show that \({\cal B}\) does not logically follow from \({\cal A}\), it suffices to demonstrate a single situation/model where \({\cal A}\) is true but \({\cal B}\) is false, no matter how many models might exist.)
The more practical way to show that \({\cal B}\) follows logically from \({\cal A}\), rather than considering all possible models, is to show that there is a step-by-step proof of \({\cal B}\) from \({\cal A}\), such that each step of the proof preserves truth.
Definition
We say that assumptions \({\cal A}_1,\ldots,{\cal A}_n\) prove a conclusion \({\cal B}\) if we can validate the conclusion using the assumptions and a fixed set of rules. In this case we write \[ {\cal A}_1,\ldots,{\cal A}_n \ \vdash \ {\cal B} \]
Of course, we want to know that what we can prove is the same as what is true. To verify that, we need to be precise about what counts as a proof (just as we gave precise definitions for what counts as a WFF, and when a WFF is true).
Definition
A Proof System is formal definition of what counts as a step-by-step proof.
In most cases, we can define a proof system by specifying a collection of rules, each of which is allowed as a single step in the proof. If so, we often describe the rule with the following notation: \[\large \frac{ \mathrm{Premise}_1 \quad \cdots \quad \mathrm{Premise}_n }{ \mathrm{Conclusion} } \] meaning that “if we already know that the premises are true, then we can immediately (in one step) assert the conclusion is true.”
We can think of a proof system as a toolbox for building proofs. In the real world, we might get by with a toolbox with just a few tools (e.g., multitools good for many purposes), or with lots of tools (e.g., specialized tools for specialized tasks). Similarly, logicians have defined and studied many different proof systems: Hilbert Systems, Natural Deduction, Resolution, and others.
Example
Here is a simple four-rule proof system known as a Hilbert System. The first rule is “Modus Ponens” (whose Latin name dates back to Medieval philosophers) or “MP” for short:
\[ \Large \frac{ {\cal A}\to {\cal B} \qquad {\cal A} }{ {\cal B} }\mathrm{\small\ MP} \] (where \({\cal A}\) and \({\cal B}\) stand for arbitrary WFFs).
So, for example, if we are doing a formal proof in a Hilbert System and we already know that \((S\lor T)\to R\) is true and that \((S\lor T)\) is true, in one step we can conclude that \(R\) must be true, and cite the MP rule as our justification.
The other rules in this proof system are “axiom schemes” whose conclusions are universally true (not dependent on having shown anything else first):
\[ \frac{}{{\cal A}\to({\cal B}\to {\cal A})}\mathrm{\small\ Ax1} \] \[ \frac{}{({\cal A}\to({\cal B}\to {\cal C}))\to(({\cal A}\to {\cal B})\to({\cal A}\to {\cal C}))}\mathrm{\small\ Ax2} \] \[ \frac{}{(\lnot {\cal B}\to\lnot {\cal A})\to({\cal A}\to {\cal B})}\mathrm{\small\ Ax3} \] So, we can assert the formula \(S\to(T\to S)\) is true (and cite A1 as our justification) at any point in a proof.
To show an example, we can verify \(P, P\to Q, Q\to R\ \vdash\ R\) in this proof system as follows:
Compared to the truth table above, this is a much simpler (and arguably more convincing) way to show that \(R\) follows from \(P\), \(P\to Q\), and \(Q\to R\).
Note that to verify this proof is correct, we just need to confirm that each step follows by one of the allowable rules of our system; there’s no need to construct (or consult) truth tables.
Why is there more than one proof system? Well, different proof systems have different strengths and weaknesses. For example, the Hilbert System above has only four rules so it is simple to explain and easy for logicians to study, but it is not at all obvious how to use these rules to prove interesting results.
Example
In the above Hilbert System, here is the shortest proof that \(\vdash P\to P\):
In contrast, Natural Deduction is a proof system with more rules, but those rules correspond more directly with typical human proof methods.
But before we turn our attention to the Natural Deduction proof system, we should ask, “How do we know if a proof system makes sense?”
For example, how do we know that the four rules in the Hilbert System above are the right rules? How do we know that don’t need a fifth rule?
Fortunately, there are two criteria that we can use.
Definition
A proof system is sound if (for all \({\cal A}_1,\ldots,{\cal A}_n,{\cal B}\)) > >\[\cal{A}_1,\ldots,\cal{A}_n \vdash \cal{B}\] > implies > \[\ \ {\cal A}_1,\ldots,{\cal A}_n \vDash {\cal B}\]
In a sound proof system, the rules are “safe” in that they won’t let us prove anything that isn’t true (that doesn’t follow logically from our assumptions.)
Putting this another way: if a conclusion is not entailed by our assumptions, we won’t be able to prove that (erroneous) conclusion if our proof system is sound.
Definition
A proof system is complete if (for all \({\cal A}_1,\ldots,{\cal A}_n,{\cal B}\)) > \[{\cal A}_1,\ldots,{\cal A}_n \vDash {\cal B}\] implies \[{\cal A}_1,\ldots,{\cal A}_n \vdash {\cal B}\]
In a complete proof system, we have enough rules to prove all conclusions that are logically entailed by our assumptions. That is, if a formula is true in every situation where our assumptions are true, we can prove this formula follows from the assumptions using step-by-step reasoning.
Example
Our Hilbert System is both sound and complete; everything we can prove with the four rules will be logically entailed by our assumptions, and all entailed conclusions have step-by-step proofs using only the four rules. > (Technically the Hilbert System is only complete for formulas written with \(\to\) and \(\lnot\). But \[{\cal C}\lor {\cal D} \ \equiv \ \lnot {\cal C}\to {\cal D}\] and \[{\cal C}\land {\cal D} \ \equiv \ \lnot({\cal C}\to \lnot {\cal D})\] so we can replace any formulas we’re interested in with logically-equivalent formulas involving only \(\to\) and \(\lnot\), and then completeness applies.)
But just because the Hilbert System rules can prove everything that is true, doesn’t mean it’s easy to find those proofs or that it’s easy to understand the proof once we’ve found it. So now we turn to Natural Deduction, a similarly sound and complete proof system that has more rules, but whose proofs are more, well, natural.
Previous: 1.6 English to WFFs